package typesys;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;

import util.Pair;

import flowlogic.STSimplifier;

import ast.AtomicLabel;
import ast.Binder;
import ast.ChannelConstant;
import ast.CstPr;
import ast.Endorse;
import ast.FunApp;
import ast.Function;
import ast.Label;
import ast.LabelConjunction;
import ast.LabelDisjunction;
import ast.Principal;
import ast.Site;
import ast.Term;
import ast.TermVar;
import ast.CompositeBinder;
import ast.Assert;
import ast.BasicBinder;

public class BinderJudgement extends TypeJudgement {
	
	private Binder binder;
	private HashMap<String, HashSet<Term>> rho;
	private Site site;
	private HashMap<String, Label> gamma;
	
	private Label ctxLabel;
	private Label derivedLabel;
	
	public BinderJudgement(
			Binder b, 
			HashMap<String, HashSet<Term>> rho, 
			Site st,
			HashMap<String, Label> g,
			PrincipalHierarchy hierarchy)
	{
		binder = b;
		this.rho = rho;
		site = st;
		gamma = g;
		setHierarchy(hierarchy);
	}

	public boolean checkAndDerive() throws FunctionUndefinedException
	{
		boolean result = false;
		
		if (binder instanceof BasicBinder) {
			
			ArrayList<Term> il = new ArrayList<Term>();
			il.add(site);
			Label siteInfl = new AtomicLabel(TopPrincipal.getInstance(), il);
			HashSet<Label> lbs = new HashSet<Label>();
			
			for (Term tc : RhoEval.eval(((BasicBinder) binder).getT(), rho)) {
				lbs.addAll(RhoEval.eval(lbc(tc), rho));
			}
			ArrayList<Label> lbsAL = new ArrayList<Label>();
			lbsAL.addAll(lbs);
			RelabellingJudgement rj = new RelabellingJudgement(
										getHierarchy(),
										siteInfl,
										new LabelConjunction(lbsAL));
			result = rj.check();
			
			HashSet<Label> lbs2 = new HashSet<Label>();
			if (result) {
				ctxLabel = new LabelConjunction(lbsAL);
				for (Term tc : RhoEval.eval(((BasicBinder) binder).getT(), rho)) {
					lbs2.addAll(RhoEval.eval(lb(tc), rho));
				}
				ArrayList<Label> lbsAL2 = new ArrayList<Label>();
				lbsAL2.addAll(lbs2);
				derivedLabel = new LabelDisjunction(lbsAL2);
			}
			
		} else if (binder instanceof CompositeBinder) {
			
			ArrayList<Binder> componentBinders = 
					((CompositeBinder) binder).getComponentBinders();
			ArrayList<Label> ctxLabelList = new ArrayList<Label>();
			ArrayList<Label> derivedLabelList = new ArrayList<Label>();
			BinderJudgement bdjgt = null;
			result = true;
			for (Binder bd : componentBinders) {
				bdjgt = new BinderJudgement(bd, rho, site, gamma, getHierarchy());
				if (!bdjgt.checkAndDerive()) {
					result = false;
					break;
				}
				ctxLabelList.add(bdjgt.getCtxLabel());
				derivedLabelList.add(bdjgt.getDerivedLabel());
			}
			if (result) {
				ctxLabel = new LabelConjunction(ctxLabelList);
				derivedLabel = new LabelDisjunction(derivedLabelList);
			}
			
		} else if (binder instanceof Assert) {
			
			Binder innerBd = ((Assert) binder).getBinder();
			BinderJudgement ibdjgt = new BinderJudgement(
					innerBd, rho, site, gamma, getHierarchy());
			Label innerCtx = null;
			if (ibdjgt.checkAndDerive()) {
				innerCtx = ibdjgt.getCtxLabel();
			}
			RelabellingJudgement rejgt = new RelabellingJudgement(
										getHierarchy(), ((Assert) binder).getL2(), innerCtx); 
			
			if (rejgt.check() && auth(((Assert) binder).getL1(), ((Assert) binder).getL2())) { 
				result = true;
				ctxLabel = ((Assert) binder).getL1();
				derivedLabel = ibdjgt.getDerivedLabel();
			}
		}
		
		return result;
	}

	public Label getCtxLabel() {
		return ctxLabel;
	}

	public Label getDerivedLabel() {
		return derivedLabel;
	}
	
	/**
	 * @param t a term that does not contain variables
	 * @return lbc_{rho,gamma}(t)
	 */
	public Label lbc(Term t) 
	{
		Label result = null;
		
		if (t instanceof Endorse) {
			result = lbc(((Endorse) t).getT());
		} else if (t instanceof FunApp) {
			Function func = STSimplifier.getFunctionMap().get(((FunApp) t).getName());
			CstPr evalRes = evalFun(func, ((FunApp) t).getArgList());
			result = lbc((Term) evalRes);
		} else {
			assert t instanceof ChannelConstant;
			result = gamma.get(((ChannelConstant) t).getName());
		}
		
		return result;
	}
	
	/**
	 * @param func
	 * @param argList with no data constants being arguments
	 * @return
	 */
	private CstPr evalFun(Function func, ArrayList<Term> argList)
	{
		CstPr result = null;
		
		ArrayList<String> argStrList = new ArrayList<String>();
		for (Term t : argList) {
			if (t instanceof CstPr) {
				argStrList.add(((CstPr) t).getName());
			} else if (t instanceof FunApp) {
				Function argFunc = 
						STSimplifier.getFunctionMap().get(((FunApp) t).getName());
				argStrList.add(evalFun(argFunc, ((FunApp) t).getArgList()).getName());
			}
		}
		
		String strResult = null;
		
		for (Pair<ArrayList<String>, String> row : func.getDefinition()) {
			if (row.getFst().equals(argStrList)) {
				strResult = row.getSnd();
				break;
			}
		}
		
		if (strResult != null) {
			result = STSimplifier.getChannelMap().get(strResult);
		}
		
		return result;
	}
	
	private boolean auth(Label l1, Label l2)
	{
		
		ArrayList<Label> lbAuthList = new ArrayList<Label>();
		ArrayList<Term> tpprSingleton = new ArrayList<Term>();
		tpprSingleton.add(TopPrincipal.getInstance());
		for (Principal p : authoritySet()) {
			lbAuthList.add(new AtomicLabel(p, tpprSingleton));
		}
		RelabellingJudgement lj2 = new RelabellingJudgement(
									getHierarchy(),
									new LabelConjunction(l1, new LabelConjunction(lbAuthList)),
									l2);
		return	lj2.check();
	}
	
	public Label lb(Term t) throws FunctionUndefinedException
	{
		Label result = null;
		
		if (t instanceof Endorse) {
			
			Label lbInner = lb(((Endorse) t).getT());
			HashSet<Label> lbs = RhoEval.eval(lbInner, rho);
			ArrayList<Label> lbsList = new ArrayList<Label>();
			lbsList.addAll(lbs);
			RelabellingJudgement lj = new RelabellingJudgement(
										getHierarchy(), 
										new LabelDisjunction(lbsList), 
										((Endorse) t).getL1());
			
			
			
			if (lj.check() && auth(((Endorse) t).getL1(), ((Endorse) t).getL2())) 
			{
				result = ((Endorse) t).getL2();
			}
			
		} else if (t instanceof FunApp) {
			
			Function func = STSimplifier.getFunctionMap().get(((FunApp) t).getName());
			CstPr evalRes = evalFun(func, ((FunApp) t).getArgList());
			result = lbc((Term) evalRes);
			
		} else if (t instanceof TermVar) {
			
			assert t instanceof ChannelConstant;
			result = gamma.get(((TermVar) t).getName());
			
		} else if (t instanceof ChannelConstant) {
			
			ChannelConstant ch = (ChannelConstant) t;
			result = gamma.get(ch.getName());
			
		}
		
		return result;
	}
	
	private HashSet<Principal> authoritySet()
	{
		HashSet<Principal> result = new HashSet<Principal>();
		result.add(site);
		HashSet<Principal> visited = new HashSet<Principal>();
		for (Principal p : site.getActsFor()) {
			result.add(p);
			result.addAll(authSetRec(p, visited));
		}
		
		return result;
	}
	
	private HashSet<Principal> authSetRec(Principal p, HashSet<Principal> visited) {
		
		HashSet<Principal> result = new HashSet<Principal>();
		
		if (visited.contains(p))
			return result;
		
		visited.add(p);
		for (Principal r : p.getActsFor()) {
			result.add(r);
			result.addAll(authSetRec(r, visited));
		}
		
		return result;
	}
	
}
